T:Type, L:(T List). L  []  (null(L)) 

latex

Definitions

b, type List, Type, t  T, s = t, x:A  B(x), P & Q, P  Q, x:AB(x), x:A. B(x), True, [], #$n, , A  B, P  Q, P  Q, xL. P(x), (x  l), hd(l), i <z j, i z j, l[i], s ~ t, A  B, a < b, x:A. B(x), [car / cdr], ||as||, n+m, i  j , i  j < k, , {x:A| B(x)} , {i..j}, , Void, False, A, A List, {T}, (xL.P(x)), x f y, f(a), A c B, a < b, a <p b, a  b, a ~ b, b | a, Dec(P), P  Q, left + right, Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), b, if a<b then c else d, n - m, tl(l)

Lemmas

l member wf, decidable false, nil member, false wf, select member, nat wf, int seg wf, member wf, non neg length, length wf1, le wf, iff wf, rev implies wf, l contains wf, l contains nil, true wf